@string(LNCS = {LNCS})
@string{SV = {Springer}}

@misc{B98,
 author = {Best, Eike and Grahlmann, Bernd},
 title = "Format descriptions",
 note = "Appendix of: PEP Documentation and User Guide 1.8. 1998. Online,
 accessed April-2013]:
 \url{http://parsys.informatik.uni-oldenburg.de/~pep/Paper/formats_all.ps.gz}",
}

@inproceedings{BBC+10,
   author    = {Paolo Baldan and Alessandro Bruni and Andrea Corradini
                and Barbara K\"onig and Stefan Schwoon},
   title     = {On the Computation of {McMillan}'s Prefix for Contextual Nets
                and Graph Grammars},
   pages     = {91--106},
   booktitle = {Proc.\ ICGT'10},
   volume    = {6372},
   series    = LNCS,
   year      = {2010}
}

@article{BCKS08,
  author    = {Paolo Baldan and Andrea Corradini
                and Barbara K\"onig and Stefan Schwoon},
  title     = {{McMillan's} complete prefix for contextual nets},
  journal   = {ToPNoC},
  year      = {2008},
  volume    = {1},
  pages     = {199--220},
  note      = {{LNCS} 5100}
}

@inproceedings{BCM98,
  author = 	 {Baldan, P. and Corradini, A. and Montanari, U.},
  title = 	 {An Event Structure Semantics for {P}/{T} Contextual Nets:
	          Asymmetric Event Structures},
  booktitle = 	 {Proc.\ FoSSaCS},
  series =       {LNCS},
  volume = 	 1378,
  year = 	 1998,
  pages = 	 {63--80},
}

@article{BCM01,
  author    = {Paolo Baldan and Andrea Corradini and Ugo Montanari},
  title     = {Contextual {Petri} nets, asymmetric event structures, and
               processes},
  journal   = {Inf.\ Comput.},
  volume    = {171},
  number    = {1},
  year      = {2001},
  pages     = {1-49},
}

@article{BFHJ03,
  author    = {Albert Benveniste and \'Eric Fabre and Stefan Haar and Claude Jard},
  journal   = {IEEE Transactions on Automatic Control},
  month     = {May},
  number    = {5},
  pages     = {714--727},
  publisher = {IEEE},
  title     = {Diagnosis of Asynchronous Discrete Event Systems: A Net Unfolding Approach},
  volume    = {48},
  year      = {2003},
}

@inproceedings{CGP00,
  author    = {Jean-Michel Couvreur and S\'ebastien Grivet and Denis Poitrenaud},
  booktitle = {Proc.\ ICATPN},
  pages     = {364--383},
  series    = {LNCS},
  title     = {Designing a {LTL} Model-Checker Based on Unfolding Graphs},
  volume    = 1825,
  year      = 2000
}

@inproceedings{CGS09,
  author    = {Michael Codish and Samir Genaim and Peter J. Stuckey},
  title     = {A declarative encoding
		of telecommunications feature subscription in {SAT}},
  pages     = {255--266},
  booktitle = {Proc.\ PPDP},
  publisher = {ACM},
  year      = {2009}
}

@inproceedings{Che10,
  author    = {Jingchao Chen},
  title     = {A new {SAT} encoding of the at-most-one constraint},
  booktitle = {Proc.\ Constraint Modelling and Reformulation},
  year      = {2010}
}

@article{Cor96,
	author = {James C. Corbett},
	title = {Evaluating Deadlock Detection Methods for Concurrent
	Software},
	journal = {IEEE Transactions on Software Engineering},
	year = {1996},
	volume = {22},
	pages = {161--180}
}

@inproceedings{CPW11,
  author    = {Jean-Michel Couvreur and Denis Poitrenaud and Pascal Weil},
  title     = {Branching processes of general {Petri} nets},
  month     = jun,
  year      = {2011},
  booktitle = {Proc.\ ICATPN},
  series    = LNCS,
  volume    = 6709,
  pages     = {129--148},
}

@misc{Cunf,
  author    = {C\'esar Rodr\'iguez},
  title     = {\cunf},
  note = "\url{http://www.lsv.ens-cachan.fr/~rodriguez/tools/cunf/}",
}

@article{DG06,
  author    = {Volker Diekert and Paul Gastin},
  journal   = {Theoretical Computer Science},
  month     = {May},
  number    = {1-2},
  pages     = {126--135},
  publisher = {Elsevier},
  title     = {From local to global temporal logics over {M}azurkiewicz traces},
  volume    = {356},
  year      = {2006}
}

@inproceedings{EH01,
  author    = {Javier Esparza and Keijo Heljanko},
  booktitle = {Proc.\ SPIN},
  pages     = {37--56},
  series    = {LNCS},
  title     = {Implementing {LTL} Model Checking with Net Unfoldings},
  volume    = {2057},
  year      = {2001}
}

@book{EH08,
  author    = {Javier Esparza and Keijo Heljanko},
  publisher = {Springer},
  series    = {EATCS Monographs in Theoretical Computer Science},
  title     = {Unfoldings - A Partial-Order Approach to Model Checking},
  year      = {2008}
}

@article{EKS08a,
  author    = {Javier Esparza and Pradeep Kanade and Stefan Schwoon},
  title     = {A Negative Result on Depth-First Unfoldings},
  journal   = {Software Tools for Technology Transfer},
  volume    = {10},
  number    = {2},
  year      = {2008},
  pages     = {161--166}
}

@article{ERV02,
  author    = {Javier Esparza and Stefan R{\"o}mer and Walter Vogler},
  journal   = {Formal Methods in System Design},
  pages     = {285--310},
  title     = {An Improvement of {McMillan's} Unfolding Algorithm},
  volume    = {20},
  year      = {2002}
}

@article{ES01,
  author    = {Javier Esparza and Claus Schr{\"o}ter},
  title     = {Unfolding Based Algorithms for the Reachability Problem},
  journal   = {Fund.\ Inf.},
  volume    = {47},
  number    = {3-4},
  year      = {2001},
  pages     = {231--245}
}

@inproceedings{ES03,
  author    = {Niklas E{\'e}n and Niklas S{\"o}rensson},
  title     = {An Extensible {SAT}-solver},
  booktitle = {Proc.\ SAT},
  year      = {2003},
  pages     = {502--518},
  series    = {LNCS 2919}
}

@misc{GRAPH,
 author = "{Graphviz Project}",
 title = "{Graphviz -- Graph Visualization Software}",
 note = "\url{http://theoretica.informatik.uni-oldenburg.de/~pep/}",
}

@article{Haa10,
  author    = {Stefan Haar},
  journal   = {IEEE Transactions on Automatic Control},
  month     = {October},
  number    = {10},
  pages     = {2310--2320},
  publisher = {IEEE Computer Society Press},
  title     = {Types of Asynchronous Diagnosability and
		the {Reveals}-Relation in Occurrence Nets},
  volume    = {55},
  year      = {2010},
}

@article{Hel99,
  author    = {Keijo Heljanko},
  journal   = {Fund.\ Inf.},
  number    = {3},
  pages     = {247--268},
  publisher = {IOS Press},
  title     = {Using Logic Programs with Stable Model Semantics
		to Solve Deadlock and Reachability Problems for 1-Safe {Petri} Nets},
  volume    = {37},
  year      = {1999}
}

@inproceedings{Hel99a,
  author = {Keijo Heljanko},
  title = {Minimizing finite complete prefixes},
  booktitle = {Proc.\ CS\&P},
  year = {1999},
  pages = {83--95}
}

@phdthesis{Hel99lc,
    author = {Keijo Heljanko},
    school = {Helsinki University of Technology},
    title = {Deadlock and reachability checking with finite complete prefixes},
    type = {Licentiate's thesis},
    year = {1999}
}

@phdthesis{Hel02,
  author    = {Keijo Heljanko},
  title     = {Combining Symbolic and Partial-Order Methods
                for Model-Checking 1-Safe {Petri} Nets},
  school    = {Helsinki University of Technology},
  year      = {2002}
}

@inproceedings{HRTW07,
  author    = {Sarah L. Hickmott and Jussi Rintanen
                and Sylvie Thi{\'e}baux and Langford B. White},
  title     = {Planning via {Petri} Net Unfolding},
  booktitle = {Proc.\ IJCAI},
  year      = {2007},
  pages     = {1904--1911}
}

@inproceedings{JK91,
  author    = {Ryszard Janicki and Maciej Koutny},
  title     = {Invariant Semantics of Nets with Inhibitor Arcs},
  year      = {1991},
  pages     = {317--331},
  booktitle = {Proc.\ CONCUR},
  series    = {LNCS},
  volume =     527
}

@article{JK:SIN,
    author = {Janicki,  R.  and Koutny, M.},
    title = {Semantics of Inhibitor Nets.},
    journal = {Information and Computation},
    volume = 123,
    pages = {1--16},
    year = 1995
}

@inproceedings{Kah09,
  author = {Vineet Kahlon},
  title = {Boundedness vs. Unboundedness of Lock Chains:
	Characterizing Decidability of {CFL}-Reachability
	for Threads Communicating via Locks},
  booktitle = {Proc.\ LICS},
  year      = {2009},
  pages     = {27-36}
}

@article{KK07,
  author    = {Victor Khomenko and
               Maciej Koutny},
  title     = {Verification of bounded {Petri} nets using integer programming},
  journal   = {Formal Methods in System Design},
  volume    = {30},
  number    = {2},
  year      = {2007},
  pages     = {143-176},
}

@misc{Khomenko,
  author    = {Victor Khomenko},
  howpublished = {Personal communication},
  year      = {2012}
}

@PhdThesis{Kho03,
  author = 	 {Victor Khomenko},
  title = 	 {Model Checking Based on Prefixes of {Petri} Net Unfoldings},
  school = 	 {School of Computing Science, Newcastle University},
  year = 	 2003
}

@inproceedings{KK00,
  author    = {Victor Khomenko and Maciej Koutny},
  title     = {{LP} Deadlock Checking Using Partial Order Dependencies},
  booktitle = {Proc.\ CONCUR},
  year      = {2000},
  pages     = {410--425},
  series    = {LNCS 1877}
}

@article{KKKV06,
  author    = {Victor Khomenko and Alex Kondratyev
		and Maciej Koutny and Walter Vogler},
  title     = {Merged Processes -- a New Condensed
		Representation of {Petri} Net Behaviour},
  journal   = {Act. Inf.},
  volume    = {43},
  number    = {5},
  year      = {2006},
  pages     = {307--330}
}

@inproceedings{KM11,
  author =       {V. Khomenko and A. Mokhov},
  title =        {An Algorithm for Direct Construction of Complete Merged Processes},
  booktitle =    {Proc.\ Petri Nets},
  year =         {2011},
  series =       {LNCS 6709},
  pages =        {89--108},
}

@inproceedings{KW10,
  author    = {Vineet Kahlon and Chao Wang},
  title     = {Universal Causality Graphs: A Precise Happens-Before Model
               for Detecting Bugs in Concurrent Programs},
  booktitle = {Proc.\ CAV},
  year      = {2010},
  pages     = {434-449},
  series    = {LNCS 6174}
}

@inproceedings{McM92,
  author    = {Kenneth L. McMillan},
  title     = {Using Unfoldings to Avoid the State Explosion Problem in
		the Verification of Asynchronous Circuits},
  year      = {1992},
  pages     = {164--177},
  booktitle = {Proc.\ CAV},
  series    = {LNCS 663},
}

@article{MM95,
 author = {McMillan, K. L.},
 title = {A technique of state space search based on unfolding},
 journal = {Form. Methods Syst. Des.},
 volume = {6},
 number = {1},
 year = {1995},
 issn = {0925-9856},
 pages = {45--65},
 publisher = {Kluwer Academic Publishers},
}

@misc{Mole,
 author = "Schwoon, Stefan",
 title  = {\mole Homepage},
 note   = "\url{http://www.lsv.ens-cachan.fr/~schwoon/tools/mole/}",
}

@inproceedings{MR94,
  author    = {Ugo Montanari and Francesca Rossi},
  title     = {Contextual occurrence nets and concurrent constraint programming},
  booktitle = {Dagstuhl Seminar 9301},
  series    = {LNCS},
  volume    =  776,
  pages     = {280-295},
  year      = {1994}
}

@article{MR95,
  author    = {Ugo Montanari and Francesca Rossi},
  title     = {Contextual Nets},
  journal   = {Acta Inf.},
  volume    = {32},
  number    = {6},
  year      = {1995},
  pages     = {545-596}
}

@inproceedings{MR97,
  author    = {Stefan Melzer and Stefan R\"omer},
  title     = {Deadlock Checking Using Net Unfoldings},
  year      = {1997},
  pages     = {352--363},
  booktitle = {Proc\ CAV},
  series    = {LNCS},
  volume    = {1254}
}

@inproceedings{NPW80,
 author = {Nielsen, Mogens and Plotkin, Gordon D. and Winskel, Glynn},
 title = {Petri Nets, Event Structures and Domains},
 booktitle = {Proc. of the International Sympoisum on Semantics of Concurrent Computation},
 year = {1979},
 isbn = {3-540-09511-X},
 pages = {266--284},
 address = {London, UK},
 }

@misc{PEP,
 author = "{PEP Project}",
 title = "{PEP} homepage",
 note = "\url{http://theoretica.informatik.uni-oldenburg.de/~pep/}",
}

@misc{PRCompress,
  author    = "Stefan Schwoon",
  title     = {\prcompress},
  note      = "\url{https://code.google.com/p/cunf/source/browse/tools/prcompress.c}"
}

@misc{Punf,
  author    = "Victor Khomenko",
  title     = {\punf},
  note = {\url{http://homepages.cs.ncl.ac.uk/victor.khomenko/tools/punf/}}
}

@misc{Mci2mp,
  author    = "Victor Khomenko",
  title     = {\mcitomp},
  note      = "\url{http://homepages.cs.ncl.ac.uk/victor.khomenko/tools/other/}"
}

@misc{Cmerge,
  author    = "C\'esar Rodr\'iguez",
  title     = {\cmerge},
  note      = "\url{https://code.google.com/p/cunf/source/browse/tools/cmerge.py}"
}

@book{Ray86,
  author    = {M. Raynal},
  title     = {Algorithms for Mutual Exclusion},
  publisher = {MIT Press},
  year      = {1986}
}

@phdthesis{Ris94,
  author    = {Gioia Ristori},
  title     = {Modelling Systems with Shared Resources via {Petri} Nets},
  school    = {Department of Computer Science, University of Pisa},
  year      = {1994}
}

@inproceedings{RTM04,
  author    = {Darsh P. Ranjan and Daijue Tang and Sharad Malik},
  title     = {A Comparative Study of {2QBF} Algorithms},
  booktitle = {Proc.\ SAT},
  year      = {2004}
}

@mastersthesis{Rod10,
  	author = {Rodr\'iguez, C\'esar},
  	school = {MPRI, Paris},
  	type =	{{M}aster thesis},
  	title =	{Implementation of a complete prefix unfolder for contextual nets},
  	year =	{2010},
}

@inproceedings{RSB11,
  author    = {C\'esar Rodr\'\i{}guez and Stefan Schwoon and Paolo Baldan},
  title     = {Efficient contextual unfolding},
  booktitle = {Proc.\ CONCUR},
  pages     = {342--357},
  month     = sep,
  year      = {2011},
  series    = LNCS,
  volume    = {6901}
}

@techreport{RSB11rr,
  author    = {C\'esar Rodr\'\i{}guez and Stefan Schwoon and Paolo Baldan},
  title     = {Efficient contextual unfolding},
  institution = {LSV, ENS de Cachan},
  year      = {2011},
  number    = {LSV-11-14}
}

@phdthesis{Sch06,
    author = {Claus Schr{\"o}ter},
    school = {Universit{\"a}t Stuttgart},
    title = {{Halbordnungs- und Reduktionstechniken f{\"u}r die automatische Verifikation von verteilten Systemen}},
    year = {2006}
}

@inproceedings{SR11,
  author    = {Stefan Schwoon and C\'esar Rodr\'\i{}guez},
  title     = {Construction and {SAT}-based verification
                of Contextual Unfoldings},
  booktitle = {Proc.\ DCFS},
  year      = {2011},
  pages     = {34--42},
  series    = {LNCS 6808},
  note      = {Extended abstract}
}

@incollection{V-98,
    author={Valmari,~A.},
    title={The State Explosion Problem},
    booktitle={Lectures on Petri Nets I: Basic Models},
    series=LNCS,
    volume={1491},
    pages={429--528},
    publisher=SV,
    address={Berlin Heidelberg},
    year={1998}
}

@inproceedings{VSY98,
  author    = {Walter Vogler and Alexei L. Semenov and Alexandre Yakovlev},
  title     = {Unfolding and Finite Prefix for Nets with Read Arcs},
  pages     = {501--516},
  booktitle = {Proc.\ CONCUR},
  series    = {LNCS},
  volume    = 1466,
  year      = {1998}
}

@article{Win02,
  author    = {J{\'o}zef Winkowski},
  title     = {Reachability in Contextual Nets},
  journal   = {Fund.\ Inf.},
  volume    = {51},
  number    = {1--2},
  year      = {2002},
  pages     = {235--250}
}

@inproceedings{BCH11,
   author = {Balaguer, Sandie and Chatain, Thomas and Haar, Stefan}, 
   booktitle = {Proc.\ ACSD},
   pages = {44-53}, 
   publisher = {IEEE},
   title = {Building Tight Occurrence Nets from Reveals Relations}, 
   year = {2011},
}

@article{Dij65,
 author = {Dijkstra, E. W.},
 title = {Solution of a problem in concurrent programming control},
 journal = {Commun. ACM},
 volume = {8},
 number = {9},
 month = sep,
 year = {1965},
 issn = {0001-0782},
 pages = {569ff},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@inproceedings{RS12,
  author    = {C\'esar Rodr\'\i{}guez and Stefan Schwoon},
  title     = {Verification of {Petri} {Nets} with {Read} {Arcs}},
  booktitle = {Proc.\ CONCUR},
  month     = sep,
  year      = {2012},
  series    = LNCS,
  volume    = {7454},
  pages     = {471--485},
}

@techreport{RS12rr,
  author    = {C\'esar Rodr\'\i{}guez and Stefan Schwoon},
  title     = {Verification of {Petri} {Nets} with {Read} {Arcs}},
  institution = {LSV, ENS de Cachan},
  year      = {2012},
  number    = {LSV-12-12}
}

@inproceedings{SS96,
  author    = {Jo{\~a}o P. Marques Silva and Karem A. Sakallah},
  title     = {GRASP - a new search algorithm for satisfiability},
  booktitle = {ICCAD},
  year      = {1996},
  pages     = {220-227}
}

@techreport{RSK13rr,
  author    = {C\'esar Rodr\'\i{}guez and Stefan Schwoon and Victor Khomenko},
  title     = {Contextual Merged Processes},
  institution = {LSV, ENS de Cachan},
  year      = {2013},
  number    = {LSV-13-06}
}

@article{BBCKRS12,
  author = {P. Baldan and A. Bruni and A. Corradini
		and B. K\"onig and C. Rodr\'\i{}guez
		and S. Schwoon},
  title     = {Efficient unfolding of contextual {P}etri nets},
  journal   = {Theo. Comp. Sci.},
  year      = {2012},
  volume    = {449},
  pages     = {2--22},
}

@inproceedings{BPK07,
  author    = {P. Bonet and C.M. Llado and R. Puijaner and W.J. Knottenbelt},
  title     = {{PIPE} v2.5: A {Petri} Net Tool for Performance Modelling},
  pages     = {91--106},
  booktitle = {Proc.\ CLEI 2007},
  year      = {2007}
}

@misc{Graphviz,
 author = "{Graphviz Project}",
 title = "Homepage",
 note = "\url{http://www.graphviz.org/}",
}

@misc{wiki:pn,
   author = "Wikipedia",
   title = "{Petri net --- Wikipedia{,} The Free Encyclopedia}",
   year = "2013",
   url = "\url{http://en.wikipedia.org/w/index.php?title=Petri_net&oldid=550780771}",
   note = "[Online; accessed 18-April-2013]"
 }

@article{Mur89,
    author = {Tadao Murata},
    booktitle = {Proc.\ of the IEEE},
    journal = {Proc.\ of the IEEE},
    month = apr,
    number = {4},
    pages = {541--580},
    publisher = {IEEE},
    title = {{Petri} nets: Properties, analysis and applications},
    url = {http://dx.doi.org/10.1109/5.24143},
    volume = {77},
    year = {1989}
}

@inproceedings{Sinz05,
  author    = {Carsten Sinz},
  title     = {Towards an Optimal {CNF} Encoding of Boolean Cardinality Constraints},
  booktitle = {Proc.\ CP},
  year      = {2005},
  pages     = {827-831},
}

@article{Frisch05,
  author    = {Alan M. Frisch and
               Timothy J. Peugniez and
               Anthony J. Doggett and
               Peter Nightingale},
  title     = {Solving Non-Boolean Satisfiability Problems with Stochastic
               Local Search: A Comparison of Encodings},
  journal   = {J. Autom. Reasoning},
  volume    = {35},
  number    = {1-3},
  year      = {2005},
  pages     = {143-179},
}

@inproceedings{DJJJMS12,
  author    = {Alexandre David and
               Lasse Jacobsen and
               Morten Jacobsen and
               Kenneth Yrke J{\o}rgensen and
               Mikael H. M{\o}ller and
               Jir\'{\i} Srba},
  title     = {{TAPAAL 2.0}: Integrated Development Environment for Timed-Arc
              {Petri} Nets},
  booktitle = {Proc.\ TACAS},
  year      = {2012},
  pages     = {492-497},
}

@misc{Coloane,
 author = "{Cosyverif Project}",
 title = "{Coloane Download Page}",
 note = "\url{http://www.cosyverif.org/index.php?N1=1&N2=2}",
}

@misc{Cosyverif,
 author = "{Cosyverif Project}",
 title = "{Homepage}",
 note = "\url{http://www.cosyverif.org}",
}

